\begin{tabbing}
$\forall$$n$:$\mathbb{N}$, $T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}), $x$,$y$:$T$.
\\[0ex]($x$ rel\_exp($T$; $R$; $n$) $y$)
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($\exists$$z$:$T$. ((0 $<$ $n$) c$\wedge$ (($x$ rel\_exp($T$; $R$; ($n$ {-} 1)) $z$) $\wedge$ ($z$ $R$ $y$))))\+
\\[0ex]$\vee$ (($n$ = 0 $\in$ $\mathbb{Z}$) $\wedge$ ($x$ = $y$)))
\-
\end{tabbing}